es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p:({e:es-E(es)| 
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p:({loc(e)
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p:({=
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p:({loc(e1)
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p:({ Id} 
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p:(prop{i:l}).
e2 = first e  e1.p(e)  prop{i:l} 

latex

Definitions	b, P  Q, False, A, t  T, x:A. B(x), loc(e), Id, es-E(es), x(s), prop{i:l}, x. t(x), e[e1,e2).P(e), P  Q, e2 = first e  e1.P(e), event_system{i:l}
Lemmas	event system wf, alle-between1 wf, not wf, es-E wf, Id wf, es-loc wf, es-loc-pred